\begin{tabbing}
Rusends1(${\it ds}$;$k$;$A$;$l$;${\it tg}$;$T$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=sends $k$(v:$A$) on $l$:\+
\\[0ex]tagged($\langle$${\it tg}$$,\,$$\lambda$$s$,$v$. ($f$($s$,$v$)).nil$\rangle$.nil,State(${\it ds}$),v):${\it tg}$ : $T$
\-
\end{tabbing}